open Gnsyn
open Grammar
open Lexer
open Printing
open Interp
open Sinterp

open Lexing
open Parsing
open List

let prev_val = ref N
and prev_type = ref Dynamic_Type

let pervasive_mode = ref false

let line_offset = ref 0

let rec read_term lexbuf = 
	input entry lexbuf 
and interpret_term term env type_env =
	let tau = static_interpret term type_env 
	in match term, tau with
		  Library(lib), _         -> interpret_file lib env type_env
		| Empty, _                -> exit 0
		| Syntax_Error, _         -> raise Parsing.Parse_error
		| _, Static_Type_Error(_) -> print_static_error tau term
		| _, _                    ->
			  let v = gnarly_interpret term env
			  in (match v, term with 
					Type_Error(_), _ -> print_dynamic_error v tau term
				      | _, Expression(Commit(terms)) ->
						print_definition (fst (split (fst (split terms))))
				      | _, _ -> 
						prev_val := v;
						prev_type := tau;
						print_result v tau
			     )
and interpret_repl env type_env =
	let lexbuf = from_channel stdin
	in line_offset := 0;
	while true do
		try (
			let (_, _, lnum, _) = term_range lexbuf
			in line_offset := lnum;
			print_fix ">> ";
			interpret_term (read_term lexbuf) env type_env;
		) with Parsing.Parse_error -> print_syntax_error lexbuf
	done
and interpret_string str env = 
	let lexbuf = from_string str 
	in line_offset := 0;
	try (
		let term = read_term lexbuf
		in let v = gnarly_interpret term env
		in match v with
			| Type_Error(_) -> print_dynamic_error v Dynamic_Type term; N
			| _             -> v
		) with Parse_error -> print_syntax_error lexbuf; N
and interpret_file file env type_env = 
	let lexbuf = from_channel (open_in file)
	in line_offset := 0;
	let rec read_file_terms lib func etc = 
		try (
			let term = read_term lexbuf
			in match term with 
				  Empty      -> (rev lib, rev func, rev etc)
				| Library(l) -> read_file_terms (term::lib) func etc
				| Expression(Commit(terms)) ->
					  read_file_terms lib (term::func) etc
				| Syntax_Error ->
					  (print_syntax_error lexbuf; read_file_terms lib func etc)
				| _          -> read_file_terms lib func (term::etc)
		) with Parse_error -> (print_syntax_error lexbuf; read_file_terms lib func etc)
	in let lib, func, etc = read_file_terms [] [] []
	and interp_terms term = interpret_term term env type_env
	in iter interp_terms lib;
	iter interp_terms func;
	iter interp_terms etc
and print_static_error tau term =
	print_fix ("\tStatic Type Error: " ^ (string_of_gntype tau) ^ "\n")
and print_dynamic_error v tau term =
	print_fix ("\tDynamic Type Error in term of type " ^ (string_of_gntype tau) ^ ": " ^ (string_of_gnvalue v) ^ "\n")
and print_syntax_error lexbuf  = 
	let (_, _, cline, cnum) = term_range lexbuf
	in print_fix ("\tSyntax Error in term at line " ^ (string_of_int (cline - !line_offset)) ^ ", character " ^ (string_of_int cnum) ^ "\n") 
and print_result v tau = 
	if not !(pervasive_mode) then 
		print_fix ("\t" ^ (string_of_gnvalue v) ^ "  :  " ^ (string_of_gntype tau) ^ "\n")
and print_definition ids = 
	if not !(pervasive_mode) then
		iter (fun id -> print_fix ("\t" ^ id ^ " defined\n")) ids
and term_range lexbuf = 
	let stop = lexbuf.Lexing.lex_curr_p
	and start = lexbuf.Lexing.lex_start_p
	in (start.Lexing.pos_lnum, start.Lexing.pos_cnum - start.Lexing.pos_bol, stop.Lexing.pos_lnum, 
	    stop.Lexing.pos_cnum - stop.Lexing.pos_bol)
